Nuprl Lemma : ecl-halt-type_wf
11,40
postcript
pdf
ds
:
x
:Id fp
Type,
da
:
k
:Knd fp
Type,
x
:ecl(
ds
;
da
). ecl-halt-type(
da
;
x
)
Type
latex
Definitions
Id
,
t
T
,
Type
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
Knd
,
ecl(
ds
;
da
)
,
Top
,
Valtype(
da
;
k
)
,
ecl-halt-kind(
x
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
ecl-halt-type(
da
;
x
)
Lemmas
ecl-halt-kind
wf
,
ma-valtype
wf
,
top
wf
,
ecl
wf
,
Knd
wf
,
fpf
wf
,
Id
wf
origin
ds:x:Id fp
Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-halt-type(da;x) 
Type ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-halt-type(da;x) Type T
x. t(x)x:A. B(x) B(a)